Nuprl Lemma : ecl-kinds-ecl-trans 11,40

ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(dsda).
ecl-kinds(x) = ecl-trans-ks(ecl-trans(x))  (Knd List) 
latex


Definitionsecl-add-catch(Al), ecl-add-throw(Am), reduce(fkas), Y, add-ecl-act(Am), reset-ecl-tuple(A), subtype(ST), top, guard(T), sq_type(T), combine-ecl-tuples2(ABfg), False, A, A  B, , combine-ecl-tuples(ABfg), spreadn(ua,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-base-tuple(ktest), ecl-trans-ks(v), xt(x), t  T, P  Q, prop{i:l}, ecl-trans(x), ecl-kinds(x), x:AB(x), P  Q, P  Q, ||as||, ecl-trans-tuple{i:l}(dsda), x(s)
Lemmascons one one, non neg length, top wf, length wf nat, Knd sq, le wf, lt int wf, band wf, bor wf, combine-ecl-tuples wf, append wf, ecl-trans-tuple wf, Id wf, Knd wf, fpf wf, ecl wf, nat wf, bool wf, ma-valtype wf, decl-state wf, ecl-trans wf, ecl-trans-ks wf, ecl-kinds wf, ecl-induction

origin